le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
↳ QTRS
↳ Overlay + Local Confluence
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
LE(s(x), s(y)) → LE(x, y)
EQ(s(x), s(y)) → EQ(x, y)
MINSORT(cons(x, xs)) → MIN(cons(x, xs))
MINSORT(cons(x, xs)) → MINSORT(rm(min(cons(x, xs)), cons(x, xs)))
MINSORT(cons(x, xs)) → RM(min(cons(x, xs)), cons(x, xs))
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
MIN(cons(x, cons(y, xs))) → LE(x, y)
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
RM(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
RM(x, cons(y, xs)) → EQ(x, y)
IF2(true, x, y, xs) → RM(x, xs)
IF2(false, x, y, xs) → RM(x, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LE(s(x), s(y)) → LE(x, y)
EQ(s(x), s(y)) → EQ(x, y)
MINSORT(cons(x, xs)) → MIN(cons(x, xs))
MINSORT(cons(x, xs)) → MINSORT(rm(min(cons(x, xs)), cons(x, xs)))
MINSORT(cons(x, xs)) → RM(min(cons(x, xs)), cons(x, xs))
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
MIN(cons(x, cons(y, xs))) → LE(x, y)
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
RM(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
RM(x, cons(y, xs)) → EQ(x, y)
IF2(true, x, y, xs) → RM(x, xs)
IF2(false, x, y, xs) → RM(x, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
RM(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
IF2(true, x, y, xs) → RM(x, xs)
IF2(false, x, y, xs) → RM(x, xs)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
RM(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
IF2(true, x, y, xs) → RM(x, xs)
IF2(false, x, y, xs) → RM(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
RM(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
IF2(true, x, y, xs) → RM(x, xs)
IF2(false, x, y, xs) → RM(x, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MIN(cons(x, cons(y, xs))) → IF1(le(x, y), x, y, xs)
Used ordering: Polynomial interpretation [POLO]:
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
POL(0) = 0
POL(IF1(x1, x2, x3, x4)) = 1 + x4
POL(MIN(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 0
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
IF1(true, x, y, xs) → MIN(cons(x, xs))
IF1(false, x, y, xs) → MIN(cons(y, xs))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
MINSORT(cons(x, xs)) → MINSORT(rm(min(cons(x, xs)), cons(x, xs)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
minsort(nil) → nil
minsort(cons(x, xs)) → cons(min(cons(x, xs)), minsort(rm(min(cons(x, xs)), cons(x, xs))))
min(nil) → 0
min(cons(x, nil)) → x
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(true, x, y, xs) → min(cons(x, xs))
if1(false, x, y, xs) → min(cons(y, xs))
rm(x, nil) → nil
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → rm(x, xs)
if2(false, x, y, xs) → cons(y, rm(x, xs))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
MINSORT(cons(x, xs)) → MINSORT(rm(min(cons(x, xs)), cons(x, xs)))
min(cons(x, nil)) → x
if1(true, x, y, xs) → min(cons(x, xs))
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(false, x, y, xs) → min(cons(y, xs))
if2(true, x, y, xs) → rm(x, xs)
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(false, x, y, xs) → cons(y, rm(x, xs))
rm(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
minsort(nil)
minsort(cons(x0, x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
minsort(nil)
minsort(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
MINSORT(cons(x, xs)) → MINSORT(rm(min(cons(x, xs)), cons(x, xs)))
min(cons(x, nil)) → x
if1(true, x, y, xs) → min(cons(x, xs))
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(false, x, y, xs) → min(cons(y, xs))
if2(true, x, y, xs) → rm(x, xs)
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(false, x, y, xs) → cons(y, rm(x, xs))
rm(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
POL(0) = 0
POL(MINSORT(x1)) = 2·x1
POL(cons(x1, x2)) = 1 + 2·x1 + x2
POL(eq(x1, x2)) = x2
POL(false) = 0
POL(if1(x1, x2, x3, x4)) = 2 + 2·x2 + 2·x3 + x4
POL(if2(x1, x2, x3, x4)) = 1 + 2·x3 + x4
POL(le(x1, x2)) = 1
POL(min(x1)) = x1
POL(nil) = 0
POL(rm(x1, x2)) = x2
POL(s(x1)) = 2·x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ PisEmptyProof
↳ QTRS
min(cons(x, nil)) → x
if1(true, x, y, xs) → min(cons(x, xs))
min(cons(x, cons(y, xs))) → if1(le(x, y), x, y, xs)
if1(false, x, y, xs) → min(cons(y, xs))
if2(true, x, y, xs) → rm(x, xs)
rm(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(false, x, y, xs) → cons(y, rm(x, xs))
rm(x, nil) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
min(nil)
min(cons(x0, nil))
min(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
rm(x0, nil)
rm(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
RM'(x61, cons(y50, xs30)) → IF2'(eq(x61, y50), x61, y50, xs30)
RM'(x61, cons(y50, xs30)) → EQ(x61, y50)
IF2'(false, x124, y103, xs61) → RM'(x124, xs61)
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
MIN(cons(x22, cons(y17, xs9))) → LE(x22, y17)
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
IF2(true, x48, y39, xs23) → RM(x48, xs23)
RM(x61, cons(y50, xs30)) → IF2(eq(x61, y50), x61, y50, xs30)
RM(x61, cons(y50, xs30)) → EQ(x61, y50)
EQ(s(x111), s(y92)) → EQ(x111, y92)
IF2(false, x124, y103, xs61) → RM(x124, xs61)
LE(s(x175), s(y145)) → LE(x175, y145)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
RM'(x61, cons(y50, xs30)) → IF2'(eq(x61, y50), x61, y50, xs30)
RM'(x61, cons(y50, xs30)) → EQ(x61, y50)
IF2'(false, x124, y103, xs61) → RM'(x124, xs61)
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
MIN(cons(x22, cons(y17, xs9))) → LE(x22, y17)
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
IF2(true, x48, y39, xs23) → RM(x48, xs23)
RM(x61, cons(y50, xs30)) → IF2(eq(x61, y50), x61, y50, xs30)
RM(x61, cons(y50, xs30)) → EQ(x61, y50)
EQ(s(x111), s(y92)) → EQ(x111, y92)
IF2(false, x124, y103, xs61) → RM(x124, xs61)
LE(s(x175), s(y145)) → LE(x175, y145)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x175), s(y145)) → LE(x175, y145)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x175), s(y145)) → LE(x175, y145)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x175), s(y145)) → LE(x175, y145)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x111), s(y92)) → EQ(x111, y92)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x111), s(y92)) → EQ(x111, y92)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x111), s(y92)) → EQ(x111, y92)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
RM(x61, cons(y50, xs30)) → IF2(eq(x61, y50), x61, y50, xs30)
IF2(true, x48, y39, xs23) → RM(x48, xs23)
IF2(false, x124, y103, xs61) → RM(x124, xs61)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
RM(x61, cons(y50, xs30)) → IF2(eq(x61, y50), x61, y50, xs30)
IF2(true, x48, y39, xs23) → RM(x48, xs23)
IF2(false, x124, y103, xs61) → RM(x124, xs61)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
RM(x61, cons(y50, xs30)) → IF2(eq(x61, y50), x61, y50, xs30)
IF2(true, x48, y39, xs23) → RM(x48, xs23)
IF2(false, x124, y103, xs61) → RM(x124, xs61)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MIN(cons(x22, cons(y17, xs9))) → IF1(le(x22, y17), x22, y17, xs9)
Used ordering: Polynomial interpretation [POLO]:
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
POL(0) = 0
POL(IF1(x1, x2, x3, x4)) = 1 + x4
POL(MIN(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 0
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
IF1(true, x9, y6, xs2) → MIN(cons(x9, xs2))
IF1(false, x35, y28, xs16) → MIN(cons(y28, xs16))
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
IF2'(false, x124, y103, xs61) → RM'(x124, xs61)
RM'(x61, cons(y50, xs30)) → IF2'(eq(x61, y50), x61, y50, xs30)
if2'(true, x48, y39, xs23) → true
rm'(x61, cons(y50, xs30)) → if2'(eq(x61, y50), x61, y50, xs30)
if2'(false, x124, y103, xs61) → rm'(x124, xs61)
rm'(x137, nil) → false
min(cons(x', nil)) → x'
if1(true, x9, y6, xs2) → min(cons(x9, xs2))
min(cons(x22, cons(y17, xs9))) → if1(le(x22, y17), x22, y17, xs9)
if1(false, x35, y28, xs16) → min(cons(y28, xs16))
if2(true, x48, y39, xs23) → rm(x48, xs23)
rm(x61, cons(y50, xs30)) → if2(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2(false, x124, y103, xs61) → cons(y103, rm(x124, xs61))
rm(x137, nil) → nil
le(0, y124) → true
le(s(x162), 0) → false
le(s(x175), s(y145)) → le(x175, y145)
min(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF2'(false, x124, y103, xs61) → RM'(x124, xs61)
RM'(x61, cons(y50, xs30)) → IF2'(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
if2'(true, x0, x1, x2)
rm'(x0, cons(x1, x2))
if2'(false, x0, x1, x2)
rm'(x0, nil)
min(cons(x0, nil))
if1(true, x0, x1, x2)
min(cons(x0, cons(x1, x2)))
if1(false, x0, x1, x2)
if2(true, x0, x1, x2)
rm(x0, cons(x1, x2))
if2(false, x0, x1, x2)
rm(x0, nil)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
IF2'(false, x124, y103, xs61) → RM'(x124, xs61)
RM'(x61, cons(y50, xs30)) → IF2'(eq(x61, y50), x61, y50, xs30)
eq(0, 0) → true
eq(0, s(y71)) → false
eq(s(x98), 0) → false
eq(s(x111), s(y92)) → eq(x111, y92)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs: